Nuprl Lemma : Rlist_wf
0,22
postcript
pdf
L
:Realizer List.
(
L
)
Realizer
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
(
L
)
Lemmas
reduce
wf
,
es
realizer
wf
,
Rplus
wf
,
Rnone
wf
origin
L:Realizer List. 
(L) 
Realizer L:Realizer List. (L) Realizer x:A. B(x) T(L)